the_es:ES, e, e', y:E. e' before y  before(e)  (e' <loc y) & (y <loc e) 

latex

Definitions	ES, t  T, x:A. B(x), E, (e <loc e'), Prop, P & Q, x before y  l, before(e), P  Q, P  Q, P  Q, b, , False, Unit, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), first(e), b, A, (x  l), P  Q, pred(e)
Lemmas	l member wf, es-pred-locl, member singleton, l before append iff, es-pred wf, es-locl-wellfnd, es-locl-iff, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, l before member, member-es-before, l before-es-before, l before wf, es-before wf, es-locl wf, es-E wf, event system wf